Nuprl Lemma : qmul-mul
11,40
postcript
pdf
x
,
y
:
. (
x
*
y
) ~ (
x
*
y
)
latex
Definitions
t
T
,
Top
,
tt
,
if
b
then
t
else
f
fi
,
r
*
s
,
x
:
A
.
B
(
x
)
Lemmas
isint-int
origin
x, y:
. (x * y) ~ (x * y) x, y:. (x * y) ~ (x * y) 
Tx:A. B(x)